1. ${\it xm}$ : $\forall$$P$:$\mathbb{P}$. $P$ $\vee$ ($\neg$$P$)
\\[0ex]2. $T$ : Type
\\[0ex]3. $P$ : $T$$\rightarrow\mathbb{P}$
\\[0ex]4. $\exists$$a$:$T$. $P$($a$)
\\[0ex]$\vdash$  case ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$)\} ) of inl($z$) =$>$ $z$ $\mid$ inr($w$) =$>$ "???" $\in$ $T$